package tr.edu.ege.kipler.satisfiability.syntactical;

import java.util.HashSet;
import java.util.Set;

import tr.edu.ege.kipler.satisfiability.container.UnfoldableTBox;
import tr.edu.ege.kipler.syntax.atomicformula.ConceptDefinition;
import tr.edu.ege.kipler.syntax.concept.BinaryConcept;
import tr.edu.ege.kipler.syntax.concept.ConceptName;
import tr.edu.ege.kipler.syntax.concept.ConceptVisitor;
import tr.edu.ege.kipler.syntax.concept.ModalConcept;
import tr.edu.ege.kipler.syntax.concept.Nominal;
import tr.edu.ege.kipler.syntax.concept.QualifiedNoRestriction;
import tr.edu.ege.kipler.syntax.concept.RoleQuantification;

/**
 * 
 * @author İnanç Seylan
 *
 */
public class UsedConceptNameVisitor implements ConceptVisitor {
	private Set<ConceptName> usedConcepts = new HashSet<ConceptName>();

	private UnfoldableTBox tbox;

	public UsedConceptNameVisitor(UnfoldableTBox tbox) {
		this.tbox = tbox;
	}

	public Set<ConceptName> getUsedConcepts() {
		return usedConcepts;
	}

	public void visitBinaryConcept(BinaryConcept bd) {
		UsedConceptNameVisitor visitor = new UsedConceptNameVisitor(tbox);
		bd.getLhs().accept(visitor);
		usedConcepts.addAll(visitor.getUsedConcepts());
		visitor = new UsedConceptNameVisitor(tbox);
		bd.getRhs().accept(visitor);
		usedConcepts.addAll(visitor.getUsedConcepts());
	}

	public void visitConceptName(ConceptName c) {
		ConceptName cClone = c.copy();
		if (c.isNegated()) {
			cClone.toggleNegated();
		}
		ConceptDefinition conDef = tbox.getDefinition(cClone);
		if (conDef != null) {
			UsedConceptNameVisitor visitor = new UsedConceptNameVisitor(tbox);
			conDef.getRhs().accept(visitor);
			usedConcepts.addAll(visitor.getUsedConcepts());
		} else {
			usedConcepts.add(cClone);
		}
	}

	public void visitModalConcept(ModalConcept md) {
		// TODO: think about this
	}

	public void visitQualifiedNoRestriction(QualifiedNoRestriction restriction) {
		UsedConceptNameVisitor visitor = new UsedConceptNameVisitor(tbox);
		restriction.getConcept().accept(visitor);
		usedConcepts.addAll(visitor.getUsedConcepts());
	}

	public void visitRoleQuantification(RoleQuantification restriction) {
		UsedConceptNameVisitor visitor = new UsedConceptNameVisitor(tbox);
		restriction.getConcept().accept(visitor);
		usedConcepts.addAll(visitor.getUsedConcepts());
	}

	public void visitNominal(Nominal nominal) {
		// nothing to do because a nominal does not have a concept name
	}

}
